Termination proof of /tmp/tmpYZ6vvc/Ex14

Termination of the following Term Rewriting System could not be shown:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

h(X) → g(X, X)
g(a, X) → f(b, X)
f(X, X) → h(a)
a → b

The replacement map contains the following entries:

h: {1}
g: {1}
a: empty set
f: {1}
b: empty set

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

Context-sensitive rewrite system:
The TRS R consists of the following rules:

h(X) → g(X, X)
g(a, X) → f(b, X)
f(X, X) → h(a)
a → b

The replacement map contains the following entries:

h: {1}
g: {1}
a: empty set
f: {1}
b: empty set

Using Improved CS-DPs we result in the following initial Q-CSDP problem.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

Q-restricted context-sensitive dependency pair problem:
The symbols in {h, H} are replacing on all positions.
For all symbols f in {g, f, G, F} we have µ(f) = {1}.

The ordinary context-sensitive dependency pairs DP_o are:

H(X) → G(X, X)
G(a, X) → F(b, X)
F(X, X) → H(a)
F(X, X) → A

The TRS R consists of the following rules:

h(X) → g(X, X)
g(a, X) → f(b, X)
f(X, X) → h(a)
a → b

Q is empty.

The approximation of the Context-Sensitive Dependency Graph contains 1 SCC with 1 less node.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ QCSDP

          ↳ ConvertedToQDPProblemProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

Q-restricted context-sensitive dependency pair problem:
The symbols in {h, H} are replacing on all positions.
For all symbols f in {g, f, F, G} we have µ(f) = {1}.

The TRS P consists of the following rules:

G(a, X) → F(b, X)
F(X, X) → H(a)
H(X) → G(X, X)

The TRS R consists of the following rules:

h(X) → g(X, X)
g(a, X) → f(b, X)
f(X, X) → h(a)
a → b

Q is empty.

Converted QDP Problem, but could not keep Q or minimality.

↳ CSR

  ↳ CSDependencyPairsProof

    ↳ QCSDP

      ↳ QCSDependencyGraphProof

        ↳ QCSDP

          ↳ ConvertedToQDPProblemProof

            ↳ QDP

              ↳ NonTerminationProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

F(X, X) → H(a)
G(a, X) → F(b, X)
H(X) → G(X, X)

The TRS R consists of the following rules:

h(X) → g(X, X)
g(a, X) → f(b, X)
f(X, X) → h(a)
a → b

Q is empty.
We have to consider all (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

The TRS P consists of the following rules:

F(X, X) → H(a)
G(a, X) → F(b, X)
H(X) → G(X, X)

The TRS R consists of the following rules:

h(X) → g(X, X)
g(a, X) → f(b, X)
f(X, X) → h(a)
a → b

s = H(a) evaluates to t =H(a)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Semiunifier: [ ]
Matcher: [ ]

Rewriting sequence

H(a) → G(a, a)
with rule H(X) → G(X, X) at position [] and matcher [X / a]

G(a, a) → G(a, b)
with rule a → b at position [1] and matcher [ ]

G(a, b) → F(b, b)
with rule G(a, X') → F(b, X') at position [] and matcher [X' / b]

F(b, b) → H(a)
with rule F(X, X) → H(a)

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence

All these steps are and every following step will be a correct step w.r.t to Q.

We applied the Incomplete Giesl Middeldorp transformation [11] to transform the context-sensitive TRS to a usual TRS.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

  ↳ Trivial-Transformation

Q restricted rewrite system:
The TRS R consists of the following rules:

mark(h(x1)) → hActive(mark(x1))
hActive(x1) → h(x1)
mark(g(x1, x2)) → gActive(mark(x1), x2)
gActive(x1, x2) → g(x1, x2)
mark(f(x1, x2)) → fActive(mark(x1), x2)
fActive(x1, x2) → f(x1, x2)
mark(a) → aActive
aActive → a
mark(b) → b
hActive(X) → gActive(mark(X), X)
gActive(a, X) → fActive(b, X)
fActive(X, X) → hActive(aActive)
aActive → b

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

MARK(f(x1, x2)) → MARK(x1)
MARK(g(x1, x2)) → GACTIVE(mark(x1), x2)
HACTIVE(X) → GACTIVE(mark(X), X)
MARK(h(x1)) → MARK(x1)
MARK(h(x1)) → HACTIVE(mark(x1))
FACTIVE(X, X) → HACTIVE(aActive)
GACTIVE(a, X) → FACTIVE(b, X)
FACTIVE(X, X) → AACTIVE
MARK(f(x1, x2)) → FACTIVE(mark(x1), x2)
HACTIVE(X) → MARK(X)
MARK(a) → AACTIVE
MARK(g(x1, x2)) → MARK(x1)

The TRS R consists of the following rules:

mark(h(x1)) → hActive(mark(x1))
hActive(x1) → h(x1)
mark(g(x1, x2)) → gActive(mark(x1), x2)
gActive(x1, x2) → g(x1, x2)
mark(f(x1, x2)) → fActive(mark(x1), x2)
fActive(x1, x2) → f(x1, x2)
mark(a) → aActive
aActive → a
mark(b) → b
hActive(X) → gActive(mark(X), X)
gActive(a, X) → fActive(b, X)
fActive(X, X) → hActive(aActive)
aActive → b

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

MARK(f(x1, x2)) → MARK(x1)
MARK(g(x1, x2)) → GACTIVE(mark(x1), x2)
HACTIVE(X) → GACTIVE(mark(X), X)
MARK(h(x1)) → MARK(x1)
MARK(h(x1)) → HACTIVE(mark(x1))
FACTIVE(X, X) → HACTIVE(aActive)
GACTIVE(a, X) → FACTIVE(b, X)
FACTIVE(X, X) → AACTIVE
MARK(f(x1, x2)) → FACTIVE(mark(x1), x2)
HACTIVE(X) → MARK(X)
MARK(a) → AACTIVE
MARK(g(x1, x2)) → MARK(x1)

The TRS R consists of the following rules:

mark(h(x1)) → hActive(mark(x1))
hActive(x1) → h(x1)
mark(g(x1, x2)) → gActive(mark(x1), x2)
gActive(x1, x2) → g(x1, x2)
mark(f(x1, x2)) → fActive(mark(x1), x2)
fActive(x1, x2) → f(x1, x2)
mark(a) → aActive
aActive → a
mark(b) → b
hActive(X) → gActive(mark(X), X)
gActive(a, X) → fActive(b, X)
fActive(X, X) → hActive(aActive)
aActive → b

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 2 less nodes.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

MARK(f(x1, x2)) → MARK(x1)
MARK(g(x1, x2)) → GACTIVE(mark(x1), x2)
HACTIVE(X) → GACTIVE(mark(X), X)
MARK(h(x1)) → MARK(x1)
MARK(h(x1)) → HACTIVE(mark(x1))
FACTIVE(X, X) → HACTIVE(aActive)
GACTIVE(a, X) → FACTIVE(b, X)
MARK(f(x1, x2)) → FACTIVE(mark(x1), x2)
MARK(g(x1, x2)) → MARK(x1)
HACTIVE(X) → MARK(X)

The TRS R consists of the following rules:

mark(h(x1)) → hActive(mark(x1))
hActive(x1) → h(x1)
mark(g(x1, x2)) → gActive(mark(x1), x2)
gActive(x1, x2) → g(x1, x2)
mark(f(x1, x2)) → fActive(mark(x1), x2)
fActive(x1, x2) → f(x1, x2)
mark(a) → aActive
aActive → a
mark(b) → b
hActive(X) → gActive(mark(X), X)
gActive(a, X) → fActive(b, X)
fActive(X, X) → hActive(aActive)
aActive → b

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

MARK(f(x1, x2)) → MARK(x1)
MARK(g(x1, x2)) → GACTIVE(mark(x1), x2)
MARK(h(x1)) → MARK(x1)
MARK(h(x1)) → HACTIVE(mark(x1))
MARK(f(x1, x2)) → FACTIVE(mark(x1), x2)
MARK(g(x1, x2)) → MARK(x1)

The remaining pairs can at least be oriented weakly.

HACTIVE(X) → GACTIVE(mark(X), X)
FACTIVE(X, X) → HACTIVE(aActive)
GACTIVE(a, X) → FACTIVE(b, X)
HACTIVE(X) → MARK(X)

Used ordering: Polynomial interpretation [25]:

POL(FACTIVE(x₁, x₂)) = 0
POL(GACTIVE(x₁, x₂)) = 0
POL(HACTIVE(x₁)) = x₁
POL(MARK(x₁)) = x₁
POL(a) = 0
POL(aActive) = 0
POL(b) = 0
POL(f(x₁, x₂)) = 1 + x₁
POL(fActive(x₁, x₂)) = 1 + x₁
POL(g(x₁, x₂)) = 1 + x₁
POL(gActive(x₁, x₂)) = 1 + x₁
POL(h(x₁)) = 1 + x₁
POL(hActive(x₁)) = 1 + x₁
POL(mark(x₁)) = x₁

The following usable rules [17] were oriented:

mark(f(x1, x2)) → fActive(mark(x1), x2)
gActive(x1, x2) → g(x1, x2)
mark(a) → aActive
fActive(x1, x2) → f(x1, x2)
mark(b) → b
aActive → a
gActive(a, X) → fActive(b, X)
fActive(X, X) → hActive(aActive)
hActive(X) → gActive(mark(X), X)
mark(h(x1)) → hActive(mark(x1))
mark(g(x1, x2)) → gActive(mark(x1), x2)
hActive(x1) → h(x1)
aActive → b

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

HACTIVE(X) → GACTIVE(mark(X), X)
FACTIVE(X, X) → HACTIVE(aActive)
GACTIVE(a, X) → FACTIVE(b, X)
HACTIVE(X) → MARK(X)

The TRS R consists of the following rules:

mark(h(x1)) → hActive(mark(x1))
hActive(x1) → h(x1)
mark(g(x1, x2)) → gActive(mark(x1), x2)
gActive(x1, x2) → g(x1, x2)
mark(f(x1, x2)) → fActive(mark(x1), x2)
fActive(x1, x2) → f(x1, x2)
mark(a) → aActive
aActive → a
mark(b) → b
hActive(X) → gActive(mark(X), X)
gActive(a, X) → fActive(b, X)
fActive(X, X) → hActive(aActive)
aActive → b

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

  ↳ Trivial-Transformation

Q DP problem:
The TRS P consists of the following rules:

HACTIVE(X) → GACTIVE(mark(X), X)
FACTIVE(X, X) → HACTIVE(aActive)
GACTIVE(a, X) → FACTIVE(b, X)

The TRS R consists of the following rules:

mark(h(x1)) → hActive(mark(x1))
hActive(x1) → h(x1)
mark(g(x1, x2)) → gActive(mark(x1), x2)
gActive(x1, x2) → g(x1, x2)
mark(f(x1, x2)) → fActive(mark(x1), x2)
fActive(x1, x2) → f(x1, x2)
mark(a) → aActive
aActive → a
mark(b) → b
hActive(X) → gActive(mark(X), X)
gActive(a, X) → fActive(b, X)
fActive(X, X) → hActive(aActive)
aActive → b

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We applied the Trivial transformation to transform the context-sensitive TRS to a usual TRS.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

h(X) → g(X, X)
g(a, X) → f(b, X)
f(X, X) → h(a)
a → b

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

F(X, X) → H(a)
G(a, X) → F(b, X)
F(X, X) → A
H(X) → G(X, X)

The TRS R consists of the following rules:

h(X) → g(X, X)
g(a, X) → f(b, X)
f(X, X) → h(a)
a → b

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

F(X, X) → H(a)
G(a, X) → F(b, X)
F(X, X) → A
H(X) → G(X, X)

The TRS R consists of the following rules:

h(X) → g(X, X)
g(a, X) → f(b, X)
f(X, X) → h(a)
a → b

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ CSR

  ↳ CSDependencyPairsProof

  ↳ Incomplete Giesl Middeldorp-Transformation

  ↳ Trivial-Transformation

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

F(X, X) → H(a)
G(a, X) → F(b, X)
H(X) → G(X, X)

The TRS R consists of the following rules:

h(X) → g(X, X)
g(a, X) → f(b, X)
f(X, X) → h(a)
a → b

Q is empty.
We have to consider all minimal (P,Q,R)-chains.